(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(define-fun _2 () Bool false)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp12| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp16@2| () Real)
(declare-fun |main::tmp@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp27| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp21| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp17| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp8@3| () Real)
(declare-fun ldv_spin@2 () Real)
(declare-fun *unsigned_int@1 (Real) Real)
(declare-fun __ADDRESS_OF_ldv_spin () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp24@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp13@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp7@3| () Real)
(declare-fun |main::var_vp3054_bit_setsda_1_p1@2| () Real)
(declare-fun |__ADDRESS_OF_main::var_vp3054_bit_setsda_1_p1| () Real)
(declare-fun |*(struct_vp3054_i2c_state)*@1| (Real) Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp21@2| () Real)
(declare-fun |__ADDRESS_OF_main::tmp| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp9| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp10@3| () Real)
(declare-fun _&_ (Real Real) Real)
(declare-fun |readl::__retval__@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp6@3| () Real)
(declare-fun *unsigned_int@2 (Real) Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp24@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp26| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp9@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp18@2| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp20| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp15@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp16| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp11@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp25@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp26@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp15@2| () Real)
(declare-fun |main::var_vp3054_bit_setsda_1_p0@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp10@2| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::dev| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp6| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp17@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp22@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp23@2| () Real)
(declare-fun |__ADDRESS_OF_main::tmp___0| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp8| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp9@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::vp3054_i2c| () Real)
(declare-fun __ADDRESS_OF_vp3054_i2c_algo_template () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp12@3| () Real)
(declare-fun |vp3054_bit_setsda::data@2| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp23| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp25| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp19| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp20@2| () Real)
(declare-fun _!!_ (Real Real) Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp15| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp20@3| () Real)
(declare-fun |vp3054_bit_setsda::dev@3| () Real)
(declare-fun |__ADDRESS_OF_main::var_vp3054_bit_setscl_0_p1| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp23@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp8@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp17@2| () Real)
(declare-fun *unsigned_int@3 (Real) Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp26@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp19@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp13@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp11| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp18@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp25@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp14@2| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp22| () Real)
(declare-fun |vp3054_bit_setsda::state@2| () Real)
(declare-fun |__ADDRESS_OF_main::var_vp3054_bit_setsda_1_p0| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp24| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp7| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp27@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp18| () Real)
(declare-fun |vp3054_bit_setsda::vp3054_i2c@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp22@2| () Real)
(declare-fun |main::tmp___0@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp14| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp11@3| () Real)
(declare-fun __ADDRESS_OF___this_module () Real)
(declare-fun |__ADDRESS_OF_main::var_vp3054_bit_setscl_0_p0| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp21@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp19@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp16@3| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp10| () Real)
(declare-fun |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp13| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp14@3| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp12@2| () Real)
(declare-fun |vp3054_bit_setsda::__cil_tmp27@2| () Real)
(declare-fun |readl::ret@1| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF___this_module)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Bool (<= _8 _7))
(define-fun _12 () Bool (not _11))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real __ADDRESS_OF_vp3054_i2c_algo_template)
(define-fun _15 () Real (__BASE_ADDRESS_OF__ _14))
(define-fun _16 () Bool (= _14 _15))
(define-fun _19 () Real (- 581))
(define-fun _20 () Bool (<= _8 _19))
(define-fun _21 () Bool (not _20))
(define-fun _22 () Real (- 1))
(define-fun _23 () Real (* (- 1) _14))
(define-fun _24 () Real (+ _8 _23))
(define-fun _25 () Bool (<= _24 _19))
(define-fun _26 () Bool (and _21 _25))
(define-fun _27 () Bool (and _16 _26))
(define-fun _28 () Bool (and _13 _27))
(define-fun _29 () Real __ADDRESS_OF_ldv_spin)
(define-fun _30 () Real (__BASE_ADDRESS_OF__ _29))
(define-fun _31 () Bool (= _29 _30))
(define-fun _32 () Real ldv_spin@2)
(define-fun _33 () Bool (= _32 _7))
(define-fun _34 () Bool (and _31 _33))
(define-fun _35 () Bool (and _28 _34))
(define-fun _36 () Real |__ADDRESS_OF_main::var_vp3054_bit_setsda_1_p0|)
(define-fun _37 () Real (__BASE_ADDRESS_OF__ _36))
(define-fun _38 () Bool (= _36 _37))
(define-fun _39 () Bool (and _35 _38))
(define-fun _40 () Real |__ADDRESS_OF_main::var_vp3054_bit_setsda_1_p1|)
(define-fun _41 () Real (__BASE_ADDRESS_OF__ _40))
(define-fun _42 () Bool (= _40 _41))
(define-fun _43 () Bool (and _39 _42))
(define-fun _44 () Real |__ADDRESS_OF_main::var_vp3054_bit_setscl_0_p0|)
(define-fun _45 () Real (__BASE_ADDRESS_OF__ _44))
(define-fun _46 () Bool (= _44 _45))
(define-fun _47 () Bool (and _43 _46))
(define-fun _48 () Real |__ADDRESS_OF_main::var_vp3054_bit_setscl_0_p1|)
(define-fun _49 () Real (__BASE_ADDRESS_OF__ _48))
(define-fun _50 () Bool (= _48 _49))
(define-fun _51 () Bool (and _47 _50))
(define-fun _52 () Real |__ADDRESS_OF_main::tmp|)
(define-fun _53 () Real (__BASE_ADDRESS_OF__ _52))
(define-fun _54 () Bool (= _52 _53))
(define-fun _55 () Bool (and _51 _54))
(define-fun _56 () Real |__ADDRESS_OF_main::tmp___0|)
(define-fun _57 () Real (__BASE_ADDRESS_OF__ _56))
(define-fun _58 () Bool (= _56 _57))
(define-fun _59 () Bool (and _55 _58))
(define-fun _61 () Real |main::tmp___0@3|)
(define-fun _62 () Bool (= _61 _7))
(define-fun _63 () Bool (not _62))
(define-fun _66 () Bool (and _59 _63))
(define-fun _69 () Real |main::tmp@3|)
(define-fun _70 () Bool (= _69 _7))
(define-fun _72 () Bool (and _66 _70))
(define-fun _75 () Real |main::var_vp3054_bit_setsda_1_p0@2|)
(define-fun _76 () Real |vp3054_bit_setsda::data@2|)
(define-fun _77 () Bool (= _75 _76))
(define-fun _78 () Real |main::var_vp3054_bit_setsda_1_p1@2|)
(define-fun _79 () Real |vp3054_bit_setsda::state@2|)
(define-fun _80 () Bool (= _78 _79))
(define-fun _81 () Bool (and _77 _80))
(define-fun _82 () Bool (and _72 _81))
(define-fun _83 () Real |__ADDRESS_OF_vp3054_bit_setsda::dev|)
(define-fun _84 () Real (__BASE_ADDRESS_OF__ _83))
(define-fun _85 () Bool (= _83 _84))
(define-fun _86 () Bool (and _82 _85))
(define-fun _87 () Real |__ADDRESS_OF_vp3054_bit_setsda::vp3054_i2c|)
(define-fun _88 () Real (__BASE_ADDRESS_OF__ _87))
(define-fun _89 () Bool (= _87 _88))
(define-fun _90 () Bool (and _86 _89))
(define-fun _91 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp6|)
(define-fun _92 () Real (__BASE_ADDRESS_OF__ _91))
(define-fun _93 () Bool (= _91 _92))
(define-fun _94 () Bool (and _90 _93))
(define-fun _95 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp7|)
(define-fun _96 () Real (__BASE_ADDRESS_OF__ _95))
(define-fun _97 () Bool (= _95 _96))
(define-fun _98 () Bool (and _94 _97))
(define-fun _99 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp8|)
(define-fun _100 () Real (__BASE_ADDRESS_OF__ _99))
(define-fun _101 () Bool (= _99 _100))
(define-fun _102 () Bool (and _98 _101))
(define-fun _103 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp9|)
(define-fun _104 () Real (__BASE_ADDRESS_OF__ _103))
(define-fun _105 () Bool (= _103 _104))
(define-fun _106 () Bool (and _102 _105))
(define-fun _107 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp10|)
(define-fun _108 () Real (__BASE_ADDRESS_OF__ _107))
(define-fun _109 () Bool (= _107 _108))
(define-fun _110 () Bool (and _106 _109))
(define-fun _111 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp11|)
(define-fun _112 () Real (__BASE_ADDRESS_OF__ _111))
(define-fun _113 () Bool (= _111 _112))
(define-fun _114 () Bool (and _110 _113))
(define-fun _115 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp12|)
(define-fun _116 () Real (__BASE_ADDRESS_OF__ _115))
(define-fun _117 () Bool (= _115 _116))
(define-fun _118 () Bool (and _114 _117))
(define-fun _119 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp13|)
(define-fun _120 () Real (__BASE_ADDRESS_OF__ _119))
(define-fun _121 () Bool (= _119 _120))
(define-fun _122 () Bool (and _118 _121))
(define-fun _123 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp14|)
(define-fun _124 () Real (__BASE_ADDRESS_OF__ _123))
(define-fun _125 () Bool (= _123 _124))
(define-fun _126 () Bool (and _122 _125))
(define-fun _127 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp15|)
(define-fun _128 () Real (__BASE_ADDRESS_OF__ _127))
(define-fun _129 () Bool (= _127 _128))
(define-fun _130 () Bool (and _126 _129))
(define-fun _131 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp16|)
(define-fun _132 () Real (__BASE_ADDRESS_OF__ _131))
(define-fun _133 () Bool (= _131 _132))
(define-fun _134 () Bool (and _130 _133))
(define-fun _135 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp17|)
(define-fun _136 () Real (__BASE_ADDRESS_OF__ _135))
(define-fun _137 () Bool (= _135 _136))
(define-fun _138 () Bool (and _134 _137))
(define-fun _139 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp18|)
(define-fun _140 () Real (__BASE_ADDRESS_OF__ _139))
(define-fun _141 () Bool (= _139 _140))
(define-fun _142 () Bool (and _138 _141))
(define-fun _143 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp19|)
(define-fun _144 () Real (__BASE_ADDRESS_OF__ _143))
(define-fun _145 () Bool (= _143 _144))
(define-fun _146 () Bool (and _142 _145))
(define-fun _147 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp20|)
(define-fun _148 () Real (__BASE_ADDRESS_OF__ _147))
(define-fun _149 () Bool (= _147 _148))
(define-fun _150 () Bool (and _146 _149))
(define-fun _151 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp21|)
(define-fun _152 () Real (__BASE_ADDRESS_OF__ _151))
(define-fun _153 () Bool (= _151 _152))
(define-fun _154 () Bool (and _150 _153))
(define-fun _155 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp22|)
(define-fun _156 () Real (__BASE_ADDRESS_OF__ _155))
(define-fun _157 () Bool (= _155 _156))
(define-fun _158 () Bool (and _154 _157))
(define-fun _159 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp23|)
(define-fun _160 () Real (__BASE_ADDRESS_OF__ _159))
(define-fun _161 () Bool (= _159 _160))
(define-fun _162 () Bool (and _158 _161))
(define-fun _163 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp24|)
(define-fun _164 () Real (__BASE_ADDRESS_OF__ _163))
(define-fun _165 () Bool (= _163 _164))
(define-fun _166 () Bool (and _162 _165))
(define-fun _167 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp25|)
(define-fun _168 () Real (__BASE_ADDRESS_OF__ _167))
(define-fun _169 () Bool (= _167 _168))
(define-fun _170 () Bool (and _166 _169))
(define-fun _171 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp26|)
(define-fun _172 () Real (__BASE_ADDRESS_OF__ _171))
(define-fun _173 () Bool (= _171 _172))
(define-fun _174 () Bool (and _170 _173))
(define-fun _175 () Real |__ADDRESS_OF_vp3054_bit_setsda::__cil_tmp27|)
(define-fun _176 () Real (__BASE_ADDRESS_OF__ _175))
(define-fun _177 () Bool (= _175 _176))
(define-fun _178 () Bool (and _174 _177))
(define-fun _179 () Real |vp3054_bit_setsda::dev@3|)
(define-fun _180 () Bool (= _76 _179))
(define-fun _181 () Bool (and _178 _180))
(define-fun _182 () Real |vp3054_bit_setsda::__cil_tmp6@3|)
(define-fun _183 () Bool (= _179 _182))
(define-fun _184 () Bool (and _181 _183))
(define-fun _187 () Real |vp3054_bit_setsda::__cil_tmp7@3|)
(define-fun _188 () Real (- 960))
(define-fun _189 () Real (* (- 1) _187))
(define-fun _190 () Real (+ _182 _189))
(define-fun _191 () Bool (= _190 _188))
(define-fun _192 () Bool (and _184 _191))
(define-fun _193 () Real (|*(struct_vp3054_i2c_state)*@1| _187))
(define-fun _194 () Real |vp3054_bit_setsda::vp3054_i2c@3|)
(define-fun _195 () Bool (= _193 _194))
(define-fun _196 () Bool (and _192 _195))
(define-fun _197 () Bool (= _79 _7))
(define-fun _198 () Bool (not _197))
(define-fun _200 () Bool (and _196 _198))
(define-fun _201 () Bool (and _196 _197))
(define-fun _202 () Real |vp3054_bit_setsda::__cil_tmp18@3|)
(define-fun _203 () Bool (= _194 _202))
(define-fun _204 () Bool (and _201 _203))
(define-fun _207 () Real |vp3054_bit_setsda::__cil_tmp19@3|)
(define-fun _208 () Real (- 1728))
(define-fun _209 () Real (* (- 1) _207))
(define-fun _210 () Real (+ _202 _209))
(define-fun _211 () Bool (= _210 _208))
(define-fun _212 () Bool (and _204 _211))
(define-fun _213 () Real |vp3054_bit_setsda::__cil_tmp20@3|)
(define-fun _214 () Bool (= _194 _213))
(define-fun _215 () Bool (and _212 _214))
(define-fun _217 () Real |vp3054_bit_setsda::__cil_tmp21@3|)
(define-fun _218 () Real (* (- 1) _217))
(define-fun _219 () Real (+ _213 _218))
(define-fun _220 () Bool (= _219 _208))
(define-fun _221 () Bool (and _215 _220))
(define-fun _222 () Real (*unsigned_int@1 _217))
(define-fun _223 () Real |vp3054_bit_setsda::__cil_tmp22@3|)
(define-fun _224 () Bool (= _222 _223))
(define-fun _225 () Bool (and _221 _224))
(define-fun _226 () Real 4294967293)
(define-fun _227 () Real (_&_ _223 _226))
(define-fun _228 () Real (*unsigned_int@2 _207))
(define-fun _229 () Bool (= _227 _228))
(define-fun _230 () Bool (and _225 _229))
(define-fun _231 () Real |vp3054_bit_setsda::__cil_tmp23@3|)
(define-fun _232 () Bool (= _194 _231))
(define-fun _233 () Bool (and _230 _232))
(define-fun _235 () Real |vp3054_bit_setsda::__cil_tmp24@3|)
(define-fun _236 () Real (* (- 1) _235))
(define-fun _237 () Real (+ _231 _236))
(define-fun _238 () Bool (= _237 _208))
(define-fun _239 () Bool (and _233 _238))
(define-fun _240 () Real |vp3054_bit_setsda::__cil_tmp25@3|)
(define-fun _241 () Bool (= _194 _240))
(define-fun _242 () Bool (and _239 _241))
(define-fun _244 () Real |vp3054_bit_setsda::__cil_tmp26@3|)
(define-fun _245 () Real (* (- 1) _244))
(define-fun _246 () Real (+ _240 _245))
(define-fun _247 () Bool (= _246 _208))
(define-fun _248 () Bool (and _242 _247))
(define-fun _249 () Real (*unsigned_int@2 _244))
(define-fun _250 () Real |vp3054_bit_setsda::__cil_tmp27@3|)
(define-fun _251 () Bool (= _249 _250))
(define-fun _252 () Bool (and _248 _251))
(define-fun _253 () Real 512)
(define-fun _254 () Real (_!!_ _250 _253))
(define-fun _255 () Real (*unsigned_int@3 _235))
(define-fun _256 () Bool (= _254 _255))
(define-fun _257 () Bool (and _252 _256))
(define-fun _258 () Real |vp3054_bit_setsda::__cil_tmp8@3|)
(define-fun _259 () Bool (= _194 _258))
(define-fun _260 () Bool (and _200 _259))
(define-fun _262 () Real |vp3054_bit_setsda::__cil_tmp9@3|)
(define-fun _263 () Real (* (- 1) _262))
(define-fun _264 () Real (+ _258 _263))
(define-fun _265 () Bool (= _264 _208))
(define-fun _266 () Bool (and _260 _265))
(define-fun _267 () Real |vp3054_bit_setsda::__cil_tmp10@3|)
(define-fun _268 () Bool (= _194 _267))
(define-fun _269 () Bool (and _266 _268))
(define-fun _271 () Real |vp3054_bit_setsda::__cil_tmp11@3|)
(define-fun _272 () Real (* (- 1) _271))
(define-fun _273 () Real (+ _267 _272))
(define-fun _274 () Bool (= _273 _208))
(define-fun _275 () Bool (and _269 _274))
(define-fun _276 () Real (*unsigned_int@1 _271))
(define-fun _277 () Real |vp3054_bit_setsda::__cil_tmp12@3|)
(define-fun _278 () Bool (= _276 _277))
(define-fun _279 () Bool (and _275 _278))
(define-fun _280 () Real 2)
(define-fun _281 () Real (_!!_ _277 _280))
(define-fun _282 () Real (*unsigned_int@2 _262))
(define-fun _283 () Bool (= _281 _282))
(define-fun _284 () Bool (and _279 _283))
(define-fun _285 () Real |vp3054_bit_setsda::__cil_tmp13@3|)
(define-fun _286 () Bool (= _194 _285))
(define-fun _287 () Bool (and _284 _286))
(define-fun _289 () Real |vp3054_bit_setsda::__cil_tmp14@3|)
(define-fun _290 () Real (* (- 1) _289))
(define-fun _291 () Real (+ _285 _290))
(define-fun _292 () Bool (= _291 _208))
(define-fun _293 () Bool (and _287 _292))
(define-fun _294 () Real |vp3054_bit_setsda::__cil_tmp15@3|)
(define-fun _295 () Bool (= _194 _294))
(define-fun _296 () Bool (and _293 _295))
(define-fun _298 () Real |vp3054_bit_setsda::__cil_tmp16@3|)
(define-fun _299 () Real (* (- 1) _298))
(define-fun _300 () Real (+ _294 _299))
(define-fun _301 () Bool (= _300 _208))
(define-fun _302 () Bool (and _296 _301))
(define-fun _303 () Real (*unsigned_int@2 _298))
(define-fun _304 () Real |vp3054_bit_setsda::__cil_tmp17@3|)
(define-fun _305 () Bool (= _303 _304))
(define-fun _306 () Bool (and _302 _305))
(define-fun _307 () Real 4294966783)
(define-fun _308 () Real (_&_ _304 _307))
(define-fun _309 () Real (*unsigned_int@3 _289))
(define-fun _310 () Bool (= _308 _309))
(define-fun _311 () Bool (and _306 _310))
(define-fun _312 () Real |vp3054_bit_setsda::__cil_tmp10@2|)
(define-fun _313 () Bool (= _267 _312))
(define-fun _314 () Real |vp3054_bit_setsda::__cil_tmp11@2|)
(define-fun _315 () Bool (= _271 _314))
(define-fun _316 () Bool (and _313 _315))
(define-fun _317 () Real |vp3054_bit_setsda::__cil_tmp12@2|)
(define-fun _318 () Bool (= _277 _317))
(define-fun _319 () Bool (and _316 _318))
(define-fun _320 () Real |vp3054_bit_setsda::__cil_tmp13@2|)
(define-fun _321 () Bool (= _285 _320))
(define-fun _322 () Bool (and _319 _321))
(define-fun _323 () Real |vp3054_bit_setsda::__cil_tmp14@2|)
(define-fun _324 () Bool (= _289 _323))
(define-fun _325 () Bool (and _322 _324))
(define-fun _326 () Real |vp3054_bit_setsda::__cil_tmp15@2|)
(define-fun _327 () Bool (= _294 _326))
(define-fun _328 () Bool (and _325 _327))
(define-fun _329 () Real |vp3054_bit_setsda::__cil_tmp16@2|)
(define-fun _330 () Bool (= _298 _329))
(define-fun _331 () Bool (and _328 _330))
(define-fun _332 () Real |vp3054_bit_setsda::__cil_tmp17@2|)
(define-fun _333 () Bool (= _304 _332))
(define-fun _334 () Bool (and _331 _333))
(define-fun _335 () Real |vp3054_bit_setsda::__cil_tmp18@2|)
(define-fun _336 () Bool (= _202 _335))
(define-fun _337 () Real |vp3054_bit_setsda::__cil_tmp19@2|)
(define-fun _338 () Bool (= _207 _337))
(define-fun _339 () Bool (and _336 _338))
(define-fun _340 () Real |vp3054_bit_setsda::__cil_tmp20@2|)
(define-fun _341 () Bool (= _213 _340))
(define-fun _342 () Bool (and _339 _341))
(define-fun _343 () Real |vp3054_bit_setsda::__cil_tmp21@2|)
(define-fun _344 () Bool (= _217 _343))
(define-fun _345 () Bool (and _342 _344))
(define-fun _346 () Real |vp3054_bit_setsda::__cil_tmp22@2|)
(define-fun _347 () Bool (= _223 _346))
(define-fun _348 () Bool (and _345 _347))
(define-fun _349 () Real |vp3054_bit_setsda::__cil_tmp23@2|)
(define-fun _350 () Bool (= _231 _349))
(define-fun _351 () Bool (and _348 _350))
(define-fun _352 () Real |vp3054_bit_setsda::__cil_tmp24@2|)
(define-fun _353 () Bool (= _235 _352))
(define-fun _354 () Bool (and _351 _353))
(define-fun _355 () Real |vp3054_bit_setsda::__cil_tmp25@2|)
(define-fun _356 () Bool (= _240 _355))
(define-fun _357 () Bool (and _354 _356))
(define-fun _358 () Real |vp3054_bit_setsda::__cil_tmp26@2|)
(define-fun _359 () Bool (= _244 _358))
(define-fun _360 () Bool (and _357 _359))
(define-fun _361 () Real |vp3054_bit_setsda::__cil_tmp27@2|)
(define-fun _362 () Bool (= _250 _361))
(define-fun _363 () Bool (and _360 _362))
(define-fun _364 () Real |vp3054_bit_setsda::__cil_tmp8@2|)
(define-fun _365 () Bool (= _258 _364))
(define-fun _366 () Bool (and _334 _365))
(define-fun _367 () Real |vp3054_bit_setsda::__cil_tmp9@2|)
(define-fun _368 () Bool (= _262 _367))
(define-fun _369 () Bool (and _366 _368))
(define-fun _370 () Bool (and _311 _363))
(define-fun _371 () Bool (and _257 _369))
(define-fun _372 () Bool (or _370 _371))
(define-fun _373 () Real |readl::ret@1|)
(define-fun _374 () Real |readl::__retval__@2|)
(define-fun _375 () Bool (= _373 _374))
(define-fun _376 () Bool (and _372 _375))


(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _376)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
